COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.SEC(Formal number theory)
C00009 00003	There are many theorems which can be proved about the properties of x and
C00010 00004	.SS(Truth,,R4:)
C00012 00005	The standard interpretation of ENT is Intuitive Number Theory (INT).  ENT is
C00015 00006
C00016 ENDMK
C⊗;
.SEC(Formal number theory)
.SS(Deductive system)
%71.%1 a countable set of symbols
.BEGIN INDENT 10,10;nofill
logical symbols: ~, ∧, ∀
variables: λa, λb, λc, ... λx, λy, λz, with or without subscripts.
constant: λ0
predicate letter: λA(λx,λy), which we write as "λx=λy".
function letters: λf(λx), λg(λx,λy), λh(λx,λy) which we write as "λx'", "λx+λy" and "λx⊗xλy", respectively.
auxiliary symbols: (, ), and ,.
.end
As before, a formal expression is any finite sequence of these
symbols.

%72.%1 We define the terms and wffs of our system as follows:

.begin tabit1(15);
\<term> ::= λ0 | <variable> | (<term>+<term>) | (<term>⊗x<term>) | <term>'
\<wff> ::= (<term>)=(<term>) | (<wff>)⊃(<wff>) | ~(<wff>) | ((∀<variable>)<wff>)
.end

The symbols ∧, ∨, and ∃ are defined as for the predicate calculus.  We
use the same conventions for elimination of parentheses in wffs, and we 
eliminate parentheses in terms ordering our function symbols (+, ⊗x, ').
We use ?A, ?B, ?C, ..., as meta-variables over wffs and ?a, ..., ?r, ?s, ..., as 
meta-variables over terms.

%73.%1 To the axioms we have from the Predicate Calculus ({yon(P7)}), we add
the following proper axioms:
.begin nofill;

	%7A6%1:   λa'=λb' ⊃ λa=λb
	%7A7%1:   ~λa'=λ0 (we will abbreviate ~?r=?s as ?r≠?s, for all terms ?r and ?s)
	%7A8%1:   λa=λb ⊃ (λa=λc ⊃ λb=λc)
	%7A9%1:   λa=λb ⊃ λa'=λb'
	%7A10%1:  λa+λ0=λa
	%7A11%1:  λa+λb'=(λa+λb)'
	%7A12%1:  λa%5x%1λ0=λ0
	%7A13%1:  λa%5x%1λb'=λa%5x%1λb+λa
	%7A14%1:  For any wff ?A(?x), ?A(λ0) ⊃ (∀?x(?A(?x)⊃?A(?x')) ⊃ ∀?x?A(?x))
.end

Note that %7A6-A13%1 are particular wffs of the system while %7A14%1 is an axiom
schema providing an infinite number of axioms.


%74.%1  We use the rules of inference ?MP and ?Gen from PC.  From %7A14%1 and
?MP we can obtain the %3Induction Rule%1 (?IR): 
.begin  tabit1(20);

\?A(λ0)     ∀?x(?A(?x)⊃?A(?x'))
\___________________________
\       ∀?x?A(?x).

.end
%7LEMMA 1%1   For any terms ?t, ?s, ?r, the following wffs are theorems of
ENT⊗↓we shall refer to the formal system of elementary number theory as ENT←:
.begin nofill;
.begin indent 15,15;
A6':   ?t'=?r' ⊃ ?t=?r
A7':   ?t'≠λ0
A8':   ?t=?r ⊃ (?t=?s ⊃ ?r=?s)
A9':   ?t=?r ⊃ ?t'=?r'
A10':  ?t+λ0=?t
A11':  ?t+?r'=(?t+?r)'
A12':  ?t%5x%1λ0=λ0
A13':  ?t%5x%1?r'=(?t%5x%1?r)+?t
.end
.end
.begin indent 10,10;
These follow from the axioms %7A6-A13%1, respectively, by first forming the
closure by means of ?Gen, and then applying %7A4%1 and ?MP with the 
appropriate terms ?t, ?s, ?r.
.end

.R9:
%7LEMMA 2%1   For any terms ?t, ?r, ?s the following wffs are theorems.
.begin nofill;indent 15,15;
a) ?t=?t
b) ?t=?r ⊃ ?r=?t
c) ?t=?r ⊃ (?r=?s ⊃ ?t=?s)
d) ?r=?t ⊃ (?s=?t ⊃ ?s=?r)
e) ?t=?r ⊃ ?t+?s=?r+?s
f) ?t=λ0+?t
g) ?t'+?r=(?t+?r)'
h) ?t+?r=?r+?t
i) ?t=?r ⊃ ?s+?t=?s+?r
j) ?t%5x%1?r=?r%5x%1?t
k) ?t=?r ⊃ ?t%5x%1?s=?r%5x%1?s
l) λ0%5x%1?t=λ0
m) ?t≠λ0 ⊃ (?s%5x%1?t=λ0 ⊃ ?s=λ0)
.end
.begin indent 10,10;
For proof see Mendelson [ ].
.end

We use the numeral λn as an abbreviation for λ0''%8...%1', where ' appears πn 
times⊗↓We will distinguish occurrences of numerals and
numbers by using different fonts. For example λ1, λ2, λ3 represent numerals; π1, π2, π3
 represent numbers.←.  
Just to see what a proof in ENT looks like, we will prove Lemma 3.

.begin nofill;group;
%7LEMMA 3%1 ##?ε?t+λ1=?t'
Proof:
.begin tabit2 (10,40);
\1) ?t+λ0'=(?t+λ0)'\Lemma 1, A6'
\2) ?t+λ0=?t\Lemma 1, A5'
\3) (?t+λ0)=?t ⊃ (?t+λ0)'=?t'\Lemma 1, A9'
\4) (?t+λ0)'=?t'\2), 3) ?MP
\5) ?t+λ0'= ?t'\1), 4) Lemma 2 c)
\6) ?t+λ1=?t'\5) abbreviation

.end
.end

.group
%7THEOREM 4%1##(reflexivity and substitutivity of =)
.begin indent 10,10;

.nofill;
1) ?ελa=λa
.fill
2) ?ελa=λb ⊃ (?A(λa,λa) ⊃ ?A(λa,λb)) where ?A(λa,λb) comes from ?A(λa,λa) by replacing
one or more occurrences of λa by λb, given that λb is free for those 
ocurrences of λa, see {yon (R7)} for definition of "free for".
.end
For proof see Mendelson [ ].
.apart



There are many theorems which can be proved about the properties of ⊗x and
+ (all the properties that we already know about multiplication and addition).
 They are not particularly pertinent to our discussion, and the
proofs in the formal system are extremely tedious.  For these reasons
they are omitted.  For examples of these see Mendelson [   ], Kleene [ ], or
Lyndon[#].

Order relations can be introduced by definitions as abbreviations for
various wffs.
.begin nofill;

	?t<?s for (∃%ew%1)(%ew%1≠λ0∧?t+%ew%1=?s)
	?t≤?s for ?t<?s ∨ ?t=?s
	?t>?s for ?s<?t
	?t≥?s for ?s≤?t

.end
.SS(Truth,,R4:)
Truth for elementary number theory is formalized as for PC, ({yonss (R8)}),
with the restriction that we have forced a partial interpretation of the 
predicate symbol =, the function symbols +, ⊗x, and ', and the constant
λ0 by our additional axioms %7A6-A14%1 (for example, = is a substitutive
equivalence relation).
Recall that a wff ?A is said
to be logically valid iff ?A is true for every interpretation.  ?A is
satisfiable iff there is an interpretaton for which ?A is satisfied
by at least one sequence of elements of the domain of interpretation.
  ?A is unsatisfiable iff ~?A is logically valid, i.e. ?A is false
for every interpretation.
The standard interpretation of ENT is Intuitive Number Theory (INT).  ENT is
consistent if there is no wff ?A such that ?ε?A and ?ε~?A, or 
equivalently, there exists an unprovable statement.  If we recognize the
standard interpretation, INT, to be a model for ENT, then of course
ENT is consistent.  However, semantic methods, involving a certain
amount of set-theoretic reasoning, are regarded by some as too
precarious to serve as a basis for consistency proofs; likewise, we will
not prove in a rigorous way that the axioms of ENT are true under the 
standard interpretation, but will take it as intuitively obvious.  Thus
when the consistency of ENT enters into the argument of a proof, we
take the statement of the consistency as an explicit, unproved assumption.

Any first order theory ⊗K is said to be ?w-%3consistent%1 iff, for every
wff ?A(?x) of ⊗K, if ?ε?A(πn) for every natural number πn, then it is not
the case that ?ε(∃?x)~?A(?x).  Again, if we accept the standard interpretation
as a model of ENT, then ENT is ?w-consistent, but we shall always explicitly
state the assumption that ENT is ?w-consistent whenever it is used in a proof.

.R6:
REMARK:  Let ⊗K be any first order theory with the same symbols as ENT.  If
⊗K is ?w-consistent, then ⊗K is consistent.
.nofill;
Proof:
.begin indent 10,10;fill;
Assume ⊗K is ?w-consistent.  Consider any wff ?A(?x) which is provable 
in ⊗K, for example, ?x=?x ⊃ ?x=?x.  In particular, ?ελn=λn ⊃ λn=λn for all
natural numbers πn.  Hence, (∃?x)~(?x=?x#⊃#?x=?x) is not provable in ⊗K.
Therefore, ⊗K is consistent.  (Since, by the tautology ~?A⊃(?A⊃?B), if
⊗K were inconsistent, every wff ?B would be provable.)
.end
.fill
If one should, for some reason, like to see a proof of consistency, there
is one in the appendix to Mendelson [ ].